Thực đơn
Luận lý Hoare Tính đúng đắn bộ phận và toàn phầnLuận lý Hoare chuẩn chỉ chứng minh tính đúng đắn bộ phận, trong khi điều kiện dừng phải được chứng minh độc lập. Do đó cách diễn dịch bộ ba Hoare là: Nếu P là trạng thái trước khi thực thi C, thì Q sẽ là trạng thái sau khi thực thi nó, hoặc C không dừng (chạy vô tận). Chú ý rằng nếu C không dừng thì sẽ không có khái niệm "sau", do đó Q có thể là bất cứ thứ gì. Thực vậy, người ta có chọn Q là false để diễn tả rằng C không dừng.
Tính đúng đắn toàn phần cũng có thể được chứng minh bằng phiên bản mở rộng của quy luật While.
Thực đơn
Luận lý Hoare Tính đúng đắn bộ phận và toàn phầnLiên quan
Luận tội Luận tội Donald Trump lần thứ hai Luận tạng Luận tội tại Hoa Kỳ Luận thuyết trung tâm Luận lý Hoare Luận ngữ Luận cứ Luận văn Luận điểm SiriTài liệu tham khảo
WikiPedia: Luận lý Hoare http://www.cs.queensu.ca/home/specsoft/ http://j-algo.binaervarianz.de/index.php?language=... http://isabelle.in.tum.de/Bali/ http://www.spatial.maine.edu/~worboys/processes/ho... //dx.doi.org/10.1145%2F363235.363259 http://www.key-project.org/download/hoare/